Nuprl Lemma : eq_id_test
11,40
postcript
pdf
("x" = "x" ~ tt) & ("x" = "y" ~ ff)
latex
Definitions
"$x"
,
a
=
b
,
IdDeq
,
eqof(
d
)
,
Atom2Deq
,
eq_atom$n(
x
;
y
)
,
P
&
Q
origin